16 BAIRE'S THEOREM AND ITS CONSEQUENCES 85
neighborhood V of 0 in E, and a real number c> 0 such that p(x) g c for all
x e x0 + V. Hence
p(z) £X*o) + P(XO + z)£c+ p(x0)
for all zeV, which proves the result (12.14.2).
(12.16.4) (Banach-Steinhaus theorem) Let E be a Frechet space, F a
normed space. Let Hbea set of continuous linear mappings ofE into F. Suppose
that sup \\u(x)\\ < + oo for alt x e E. Then H is equicontinuous.
UGH
The function p(x) = sup ||t/(.x)||, being finite for all x € E, is a seminorm
ueH
on E (12.14.1). Since each of the functions jci-»||w(jt)|| is continuous, p is
lower semicontinuous (12.7.7). The result therefore follows from (12.16.3)
and (12.15.7.1).
As a consequence, we have:
(12.16.5) (i) Under the hypotheses of (12.16.4), let (un) be a sequence of
continuous linear mappings ofE into F which converges simply in Etoa mapping
uofE into F. Then u is a continuous linear mapping ofE into F.
(ii) More generally, let Z be a metric space, A a subset ofZ, and z\~*uza
mapping of A into the space of continuous linear mappings of E into F. Let
z0 e Z be a point in the closure of A, and suppose that the limit
lim uz(x) = v(x)
Z-+ZQ, ze A
exists in F, for each xeE. Then v is a continuous linear mapping ofE into F.
(i) From the hypotheses we have sup ||z/n(x)|| < +00 for all x e E, hence
n
the Banach-Steinhaus theorem shows that the sequence («„) is equicontinuous,
and the continuity of u follows from (7.5.5). The fact that u is linear is an
immediate consequence of the principle of extension of identities.
(ii) The point z0 is the limit of a sequence of points (zn) in A (3.13.13),
hence v(x) == lim uZn(x) for all x e E. Now apply (i).
n-* oo
(12.16.6) Let E be a Fr&chet space, F a Banach space, I an open interval in R.
Let £?(E; F) denote the space of continuous linear mappings ofE into F,
endowed with the topology of simple convergence (12.15). If a mapping *h-+/f of
I into £?(E; F) is differentiable with respect to the topology of simple convergence
(12.15), then there exists a mapping fi-+/J of I into &(E; F) such that
= D(ft(x))forallxeE.point x0 e E, ace or a locally compact metrizable space (by virtue